COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	knowle[f81,jmc]		axiomatizing knowledge using consistency
C00010 ENDMK
C⊗;
knowle[f81,jmc]		axiomatizing knowledge using consistency
Oct 21, 1981

1. If we suppose that knowledge is closed under logical proof,
then proving non-knowledge carries with it a proof of
consistency.  In part this is the lesson of Boolos's "The
Unprovability of Consistency".  It may also be the lesson of
Kaplan and Montague's "A Paradox Regained" and Montague's
"Syntactic Treatments of Modality".

2. Montague and Kaplan show the inconsistency of the system
consisting of the three desirable axioms

Kp' ⊃ p

K(Kp' ⊃ p)'

K(p') ∧ I(p',q') ⊃ Kq'

given that the system contains enough machinery to do
elementary syntax.  Here  p  represents a sentence, and
p'  represents its Goedel number or its LISP quotation.

3. Among other things, we shall consider
the following weakening of the above axioms:

K(n,p') ⊃ p

K(n+1,(K(n,p') ⊃ p)')

K(n,p') ∧ I(p',q') ⊃ K(n,q').

Thus we have integer indexed levels of knowledge, and the second
axiom is a statement about knowledge at the higher level about
the soundness of the next lower level.  This proposal is akin
to the Montague-Kaplan suggestion to use levels of metalanguage,
but it is more feasible to implement.  Of course, we must face
the fact that a hierarchy of knowledge operators does not correspond
to anything in common sense psychology.  The magic of non-monotonic
reasoning may come to the rescue as we shall indicate later.

	I'll bet the above axioms are consistent, but I don't
know the technique for proving it.  It may involve some appeal
to considerations like those in Gentzen's proof of the consistency
of arithmetic.  More likely it can be done merely by interpreting
K(n,p) as the provability of  p  in the  n th  level strengthening
of arithmetic as done by Feferman.

	4. Suppose we want to prove that Mr. P does not know
the numbers initially - assuming that the numbers are 4 and 13.
We will argue that Mr. P doesn't know that the numbers aren't
2 and 26.  A similar argument will show that he doesn't know
they aren't 4 and 13.

	Mr. P knows  mn = 52.  Suppose he knew that the numbers
were 2 and 26, i.e. he could prove it from  mn = 52.  Imagine the
proof to be given.  Then by the deduction theorem or as a rule of
a natural deduction system, we could prove

	mn=52 ⊃ m=2 ∧ n=26

from no premisses at all.  But then natural deduction would allow
universal generalization giving

	∀mn.(mn=52 ⊃ m=2 ∧ n=26).

Now we can instantiate m to 4 and  n  to 13 giving

	4.13 = 52 ⊃ 4=2 ∧ 13=26

which is false.  If we can assume that Mr. P knows no falsehoods,
i.e. his knowledge is consistent, then we can deduce that Mr.
P doesn't know that m=2 and n=26.  Likewise he doesn't know
that  m=4 and n=13.

	Formalizing this argument so that it could be done
FOL or EKL may involve considerable difficulties.  It involves
formalizing the heart of the metamathematics of natural
deduction.  It would be interesting to know of the metamathematical
facilities of FOL would help.  Somehow, I am pessimistic about it.

[Afterthought: Maybe we don't need the universal generalization
and instantiation.  If we could prove m=2∧n=26 from the assumption
mn=52, then the same proof would prove 4=2∧13=26 from the assumption
(known to be true) that 4*13=52].

[Further thought: The main problem won't be the detailed deduction
starting with numbers, but the more complicated proposition that
if m0 and n0 aren't both primes, then Mr. P doesn't know that m and
n aren't m' and n' for any m' and n' such that m'*n' = m0*n0].


	5. Mr. P can make this reasoning himself provided he
puts his knowledge about knowledge into a hierarchy.  He reasons
about numbers using Peano arithmetic, but uses the axiom that
Peano arithmetic is consistent in order to conclude that he
doesn't know something.

[There are some problems here.  Why shouldn't he use the axiom
that Peano arithmetic is consistent in the initial reasoning?]

	6. Maybe we can use non-monotonic reasoning to simplify
Montague's axioms.  Namely, we may use:

Kp' ⊃ p,

¬prevented((K(Kp' ⊃ p)')') ⊃ K((Kp' ⊃ p)'),

and

Kp' ∧ I(p',q') ⊃ Kq'.

	We then circumscribe the predicate  prevented.  This lets
us draw back from any inconsistencies reached.  by optimistic
circumscription.  Oh well, we say, "his knowing the correctness
of his reasoning was prevented in this case".

Oct 31

	Everything seems to become much more complicated if we must
reason about the beliefs (it is hard to say knowledge any more) of
someone who reasons non-monotonically.